\begin{tabbing}
random{-}seq($T$;${\it sz}$;${\it eq}$;$f$)
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=$\forall$$k$:$\mathbb{N}$, $g$:($\mathbb{N}$$_{\mbox{\scriptsize $<$$k$}}$$\rightarrow\mathbb{N}$), $x$:($k$:$\mathbb{N}\times$($\mathbb{N}$$_{\mbox{\scriptsize $<$$k$}}$$\rightarrow$$T$)).\+
\\[0ex]increasing($g$;$k$) $\Rightarrow$ frequency(derived{-}seq($f$;$\langle$$k$$,\,$$g$$\rangle$);$x$) $\sim$ (1/exp(${\it sz}$;$k$))
\-
\end{tabbing}